{\rtf1\ansi\ansicpg1252\uc1\deff0
{\fonttbl{\f0\fmodern\fcharset0\fprq2 RobotoMono-SemiBold;}}
{\colortbl;\red0\green0\blue0;\red255\green255\blue255;\red128\green128\blue128;}
\paperw12240\paperh15840\margl1800\margr1800\margt1440\margb1440\f0\fs22\cf0
\pard\plain \tx0\tx360\tx720\tx1080\tx1440\tx1800\tx2160\tx2880\tx3600\tx4320\ltrch\loch {\f0\fs22\b0\i0 In order to \loch\af0\hich\af0\dbch\af0\uc1\u8220\'93reboot\u8221\'94 Synchronous Programming, we need to come up with a revised version of \u8220\'93everything happens simultaneously\u8221\'94}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 Around the same time that the first papers on synchronous programming were being written, Leslie Lamport wrote "The Temporal Logic of Actions" - it's a pretty dense research paper if you're not used to formal logic (I am not), but it lays out a framework for proving the correctness of concurrent systems - these could be threads in a process, nodes in a distributed system, or logic gates in a CPU.}
\par\plain \f0\fs22\b0\i0
\par\plain {\field{\*\fldinst HYPERLINK "https://lamport.azurewebsites.net/pubs/lamport-actions.pdf"}{\fldrslt\f0\fs22\b0\i0 https://lamport.azurewebsites.net/pubs/lamport-actions.pdf}}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 His later works defined the languages TLA+ and PlusCal, which allowed those proofs to be expressed in something more like a programming language. TLA+ and PlusCal let you describe a real-world program in terms of every possible way the state of the program could change in response to an event. Once you\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92ve built that description, you can prove (in the strong sense) that certain combinations of states are never possible or always possible or will always happen in a certain sequence, etcetera. To be clear, TLA+ and PlusCal are not programming languages, they\u8217\'92re more like \u8220\'93provable specification languages\u8221\'94 - statements like "foo will never exceed 10" can be proven or disproven using the formal methods of temporal logic (complicated). You can\u8217\'92t \u8220\'93run\u8221\'94 them in the usual sense, but you can use them as a tool for building more reliable code.}
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0}